CPAchecker Report

Find only exact matches

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

	Rank	Scope
-V-		{{line.bestrank}}		{{line.desc}}

Precondition (initial variable assignment):

{{fault.rank}}.

Details:

Current values:

Name	Value

{{sourceFiles[selectedSourceFile]}}

// This file is part of the SV-Benchmarks collection of verification tasks:  
// https://github.com/sosy-lab/sv-benchmarks  
//  
// SPDX-FileCopyrightText: 2010-2020 NIST  
// SPDX-FileCopyrightText: 2020 The SV-Benchmarks Community  
//  
// SPDX-License-Identifier: CC0-1.0  
  
/* Generated by Frama-C */  
  
typedef unsigned long size_t;  
  
typedef int wchar_t;  
  
typedef long __int64_t;  
  
typedef __int64_t int64_t;  
  
typedef unsigned int wint_t;  
  
struct _twoIntsStruct {  
   int intOne ;  
   int intTwo ;  
};  
  
typedef struct _twoIntsStruct twoIntsStruct;  
  
struct __pthread_internal_list {  
   struct __pthread_internal_list *__prev ;  
   struct __pthread_internal_list *__next ;  
};  
  
typedef struct __pthread_internal_list __pthread_list_t;  
  
struct __pthread_mutex_s {  
   int __lock ;  
   unsigned int __count ;  
   int __owner ;  
   unsigned int __nusers ;  
   int __kind ;  
   short __spins ;  
   short __elision ;  
   __pthread_list_t __list ;  
};  
  
typedef unsigned long pthread_t;  
  
union __anonunion_pthread_mutexattr_t_36 {  
   char __size[4U] ;  
   int __align ;  
};  
  
typedef union __anonunion_pthread_mutexattr_t_36 pthread_mutexattr_t;  
  
union pthread_attr_t {  
   char __size[56U] ;  
   long __align ;  
};  
  
typedef union pthread_attr_t pthread_attr_t;  
  
union __anonunion_pthread_mutex_t_38 {  
   struct __pthread_mutex_s __data ;  
   char __size[40U] ;  
   long __align ;  
};  
  
typedef union __anonunion_pthread_mutex_t_38 pthread_mutex_t;  
  
struct _stdThread;  
  
typedef struct _stdThread *stdThread;  
  
struct _stdThreadLock;  
  
typedef struct _stdThreadLock *stdThreadLock;  
  
struct _stdThread {  
   pthread_t handle ;  
   void (*start)(void *) ;  
   void *args ;  
};  
  
struct _stdThreadLock {  
   pthread_mutex_t mutex ;  
};  
  
typedef unsigned short __uint16_t;  
  
typedef unsigned int __uint32_t;  
  
typedef long __time_t;  
  
typedef long __ssize_t;  
  
typedef unsigned int __socklen_t;  
  
typedef __ssize_t ssize_t;  
  
typedef __time_t time_t;  
  
typedef __uint16_t uint16_t;  
  
typedef __uint32_t uint32_t;  
  
typedef __socklen_t socklen_t;  
  
typedef unsigned short sa_family_t;  
  
struct sockaddr {  
   sa_family_t sa_family ;  
   char sa_data[14U] ;  
};  
  
typedef uint32_t in_addr_t;  
  
struct in_addr {  
   in_addr_t s_addr ;  
};  
  
typedef uint16_t in_port_t;  
  
struct sockaddr_in {  
   sa_family_t sin_family ;  
   in_port_t sin_port ;  
   struct in_addr sin_addr ;  
   unsigned char sin_zero[8U] ;  
};  
  
int printf(char const * , ...);  
  
  
int sscanf(char const *, char const * , ...);  
  
  
int puts(char const *);  
  
  
int rand(void);  
  
  
int iswxdigit(wint_t);  
  
  
unsigned short const **__ctype_b_loc(void);  
  
  
int const GLOBAL_CONST_TRUE;  
  
  
int const GLOBAL_CONST_FALSE;  
  
  
int const GLOBAL_CONST_FIVE;  
  
  
int globalTrue;  
  
  
int globalFalse;  
  
  
int globalFive;  
  
  
void printLine(char const *line);  
  
  
void printWLine(wchar_t const *line);  
  
  
void printIntLine(int intNumber);  
  
  
void printShortLine(short shortNumber);  
  
  
void printFloatLine(float floatNumber);  
  
  
void printLongLine(long longNumber);  
  
  
void printLongLongLine(int64_t longLongIntNumber);  
  
  
void printSizeTLine(size_t sizeTNumber);  
  
  
void printHexCharLine(char charHex);  
  
  
void printWcharLine(wchar_t wideChar);  
  
  
void printUnsignedLine(unsigned int unsignedNumber);  
  
  
void printHexUnsignedCharLine(unsigned char unsignedCharacter);  
  
  
void printDoubleLine(double doubleNumber);  
  
  
void printStructLine(twoIntsStruct const *structTwoIntsStruct);  
  
  
void printBytesLine(unsigned char const *bytes, size_t numBytes);  
  
  
size_t decodeHexChars(unsigned char *bytes, size_t numBytes, char const *hex);  
  
  
size_t decodeHexWChars(unsigned char *bytes, size_t numBytes, wchar_t const *hex);  
  
  
int globalReturnsTrue(void);  
  
  
int globalReturnsFalse(void);  
  
  
int globalReturnsTrueOrFalse(void);  
  
  
int globalArgc;  
  
  
char **globalArgv;  
  
  
int wprintf(wchar_t const * , ...);  
  
  
int swscanf(wchar_t const *, wchar_t const * , ...);  
  
  
void printLine(char const *line)  
{  
    
  if (line != (char const *)0)   
                               printf("%s\n",line); else ;  
    
  return;  
}  
  
  
void printWLine(wchar_t const *line)  
{  
    
  if (line != (wchar_t const *)0)   
                                  wprintf((wchar_t const *)L"%" "l" "s" "\\n" ,line); else ;  
    
  return;  
}  
  
  
void printIntLine(int intNumber)  
{  
    
  printf("%d\n",intNumber);  
    
  return;  
}  
  
  
  
  
void printFloatLine(float floatNumber)  
{  
    
  printf("%f\n",(double)floatNumber);  
    
  return;  
}  
  
  
void printLongLine(long longNumber)  
{  
    
  printf("%ld\n",longNumber);  
    
  return;  
}  
  
  
  
  
void printSizeTLine(size_t sizeTNumber)  
{  
    
  printf("%zu\n",sizeTNumber);  
    
  return;  
}  
  
  
void printHexCharLine(char charHex)  
{  
    
  printf("%02x\n",(int)charHex);  
    
  return;  
}  
  
  
void printWcharLine(wchar_t wideChar)  
{  
  wchar_t s[2U];  
    
  s[0] = wideChar;  
    
  s[1] = 0;  
    
  printf("%ls\n",(wchar_t *)(& s));  
    
  return;  
}  
  
  
void printUnsignedLine(unsigned int unsignedNumber)  
{  
    
  printf("%u\n",unsignedNumber);  
    
  return;  
}  
  
  
void printHexUnsignedCharLine(unsigned char unsignedCharacter)  
{  
    
  printf("%02x\n",(int)unsignedCharacter);  
    
  return;  
}  
  
  
void printDoubleLine(double doubleNumber)  
{  
    
  printf("%g\n",doubleNumber);  
    
  return;  
}  
  
  
void printStructLine(twoIntsStruct const *structTwoIntsStruct)  
{  
    
  printf("%d -- %d\n",structTwoIntsStruct->intOne,structTwoIntsStruct->intTwo);  
    
  return;  
}  
  
  
void printBytesLine(unsigned char const *bytes, size_t numBytes)  
{  
  size_t i;  
    
  i = 0UL;  
    
  goto ldv_3392;  
  ldv_3391:   
  ;  
    
  printf("%02x",(int)*(bytes + i));  
    
  i += 1UL;  
  ldv_3392:   
  ;  
    
  if (i < numBytes)   
                    goto ldv_3391; else   
                                        goto ldv_3393;  
  ldv_3393:   
  ;  
    
  puts("");  
    
  return;  
}  
  
  
size_t decodeHexChars(unsigned char *bytes, size_t numBytes, char const *hex)  
{  
    
  size_t numWritten = 0UL;  
    
  goto ldv_3402;  
  ldv_3401:   
  ;  
  {  
    int byte;  
      
    sscanf(hex + numWritten * 2UL,"%02x",& byte);  
      
    *(bytes + numWritten) = (unsigned char)byte;  
      
    numWritten += 1UL;  
  }  
  ldv_3402:   
  ;  
    
  if (numWritten < numBytes) {  
    unsigned short const **tmp;  
      
    tmp = __ctype_b_loc();  
      
    ;  
      
    if (((int)*(*tmp + (int)*(hex + numWritten * 2UL)) & 4096) != 0) {  
      unsigned short const **tmp_0;  
        
      tmp_0 = __ctype_b_loc();  
        
      ;  
        
      if (((int)*(*tmp_0 + (int)*(hex + (numWritten * 2UL + (size_t)1U))) & 4096) != 0)   
          
        goto ldv_3401; else   
                            goto ldv_3403;  
    }  
    else   
         goto ldv_3403;  
  }  
  else   
       goto ldv_3403;  
  ldv_3403:   
  ;  
    
  return numWritten;  
}  
  
  
size_t decodeHexWChars(unsigned char *bytes, size_t numBytes, wchar_t const *hex)  
{  
    
  size_t numWritten = 0UL;  
    
  goto ldv_3412;  
  ldv_3411:   
  ;  
  {  
    int byte;  
      
    swscanf(hex + numWritten * 2UL,(wchar_t const *)L"%" "0" "2" "x" ,& byte);  
      
    *(bytes + numWritten) = (unsigned char)byte;  
      
    numWritten += 1UL;  
  }  
  ldv_3412:   
  ;  
    
  if (numWritten < numBytes) {  
    int tmp;  
      
    tmp = iswxdigit((unsigned int)*(hex + numWritten * 2UL));  
      
    if (tmp != 0) {  
      int tmp_0;  
        
      tmp_0 = iswxdigit((unsigned int)*(hex + (numWritten * 2UL + (size_t)1U)));  
        
      if (tmp_0 != 0)   
                      goto ldv_3411; else   
                                          goto ldv_3413;  
    }  
    else   
         goto ldv_3413;  
  }  
  else   
       goto ldv_3413;  
  ldv_3413:   
  ;  
    
  return numWritten;  
}  
  
  
int globalReturnsTrue(void)  
{  
  int __retres;  
    
  __retres = 1;  
    
  return __retres;  
}  
  
  
int globalReturnsFalse(void)  
{  
  int __retres;  
    
  __retres = 0;  
    
  return __retres;  
}  
  
  
int globalReturnsTrueOrFalse(void)  
{  
  int __retres;  
  int tmp;  
    
  tmp = rand();  
    
  __retres = tmp % 2;  
    
  return __retres;  
}  
  
  
int const GLOBAL_CONST_TRUE = 1;  
  
int const GLOBAL_CONST_FALSE = 0;  
  
int const GLOBAL_CONST_FIVE = 5;  
  
int globalTrue = 1;  
  
int globalFalse = 0;  
  
int globalFive = 5;  
  
void good1(void)  
{  
    
  return;  
}  
  
  
void good2(void)  
{  
    
  return;  
}  
  
  
void good3(void)  
{  
    
  return;  
}  
  
  
void good4(void)  
{  
    
  return;  
}  
  
  
void good5(void)  
{  
    
  return;  
}  
  
  
void good6(void)  
{  
    
  return;  
}  
  
  
void good7(void)  
{  
    
  return;  
}  
  
  
void good8(void)  
{  
    
  return;  
}  
  
  
void good9(void)  
{  
    
  return;  
}  
  
  
void bad1(void)  
{  
    
  return;  
}  
  
  
void bad2(void)  
{  
    
  return;  
}  
  
  
void bad3(void)  
{  
    
  return;  
}  
  
  
void bad4(void)  
{  
    
  return;  
}  
  
  
void bad5(void)  
{  
    
  return;  
}  
  
  
void bad6(void)  
{  
    
  return;  
}  
  
  
void bad7(void)  
{  
    
  return;  
}  
  
  
void bad8(void)  
{  
    
  return;  
}  
  
  
void bad9(void)  
{  
    
  return;  
}  
  
  
int globalArgc = 0;  
  
char **globalArgv = (char **)0;  
  
void *malloc(size_t);  
  
  
void free(void *);  
  
  
int pthread_create(pthread_t *, pthread_attr_t const *, void *(*)(void *), void *);  
  
  
void pthread_exit(void *);  
  
  
int pthread_join(pthread_t, void **);  
  
  
int pthread_mutex_init(pthread_mutex_t *, pthread_mutexattr_t const *);  
  
  
int pthread_mutex_destroy(pthread_mutex_t *);  
  
  
int pthread_mutex_lock(pthread_mutex_t *);  
  
  
int pthread_mutex_unlock(pthread_mutex_t *);  
  
  
int stdThreadCreate(void (*start)(void *), void *args, stdThread *thread);  
  
  
int stdThreadJoin(stdThread thread);  
  
  
int stdThreadDestroy(stdThread thread);  
  
  
int stdThreadLockCreate(stdThreadLock *lock);  
  
  
void stdThreadLockAcquire(stdThreadLock lock);  
  
  
void stdThreadLockRelease(stdThreadLock lock);  
  
  
void stdThreadLockDestroy(stdThreadLock lock);  
  
  
static void *internal_start(void *args)  
{  
  void *__retres;  
    
  stdThread thread = (struct _stdThread *)args;  
    
  (*(thread->start))(thread->args);  
    
  pthread_exit((void *)0);  
    
  __retres = (void *)0;  
    
  return __retres;  
}  
  
  
int stdThreadCreate(void (*start)(void *), void *args, stdThread *thread)  
{  
  int __retres;  
  pthread_t handle;  
  stdThread my_thread;  
  int tmp_0;  
    
  *thread = (struct _stdThread *)0;  
    
  my_thread = (stdThread)malloc(24UL);  
    
  if (my_thread == (struct _stdThread *)0) {  
      
    __retres = 0;  
      
    goto return_label;  
  }  
  else ;  
    
  my_thread->start = start;  
    
  my_thread->args = args;  
    
  tmp_0 = pthread_create(& handle,(pthread_attr_t const *)0,& internal_start,(void *)my_thread);  
    
  if (tmp_0 != 0) {  
      
    free((void *)my_thread);  
      
    __retres = 0;  
      
    goto return_label;  
  }  
  else ;  
    
  my_thread->handle = handle;  
    
  *thread = my_thread;  
    
  __retres = 1;  
  return_label:   
                return __retres;  
}  
  
  
int stdThreadJoin(stdThread thread)  
{  
  int __retres;  
  void *dummy;  
  int tmp;  
    
  tmp = pthread_join(thread->handle,& dummy);  
    
  if (tmp != 0) {  
      
    __retres = 0;  
      
    goto return_label;  
  }  
  else ;  
    
  __retres = 1;  
  return_label:   
                return __retres;  
}  
  
  
int stdThreadDestroy(stdThread thread)  
{  
  int __retres;  
    
  free((void *)thread);  
    
  __retres = 1;  
    
  return __retres;  
}  
  
  
int stdThreadLockCreate(stdThreadLock *lock)  
{  
  int __retres;  
  int tmp_0;  
    
  stdThreadLock my_lock = (struct _stdThreadLock *)0;  
    
  *lock = (struct _stdThreadLock *)0;  
    
  my_lock = (stdThreadLock)malloc(40UL);  
    
  if (my_lock == (struct _stdThreadLock *)0) {  
      
    __retres = 0;  
      
    goto return_label;  
  }  
  else ;  
    
  tmp_0 = pthread_mutex_init(& my_lock->mutex,(pthread_mutexattr_t const *)0);  
    
  if (tmp_0 != 0) {  
      
    free((void *)lock);  
      
    __retres = 0;  
      
    goto return_label;  
  }  
  else ;  
    
  *lock = my_lock;  
    
  __retres = 1;  
  return_label:   
                return __retres;  
}  
  
  
void stdThreadLockAcquire(stdThreadLock lock)  
{  
    
  pthread_mutex_lock(& lock->mutex);  
    
  return;  
}  
  
  
void stdThreadLockRelease(stdThreadLock lock)  
{  
    
  pthread_mutex_unlock(& lock->mutex);  
    
  return;  
}  
  
  
void stdThreadLockDestroy(stdThreadLock lock)  
{  
    
  pthread_mutex_destroy(& lock->mutex);  
    
  free((void *)lock);  
    
  return;  
}  
  
  
void ldv_exit(void);  
  
  
char *ldv_strcpy(char *dest, char const *src);  
  
  
size_t ldv_strlen(char const *str);  
  
  
unsigned long strtoul(char const *, char **, int);  
  
  
void srand(unsigned int);  
  
  
static void ldv_exit_2(int ldv_func_arg1);  
  
  
time_t time(time_t *);  
  
  
void *memset(void *, int, size_t);  
  
  
static char *ldv_strcpy_3(char * __restrict ldv_func_arg1, char const * __restrict ldv_func_arg2);  
  
  
static size_t ldv_strlen_1(char const *ldv_func_arg1);  
  
  
int socket(int, int, int);  
  
  
int connect(int, struct sockaddr const *, socklen_t);  
  
  
ssize_t recv(int, void *, size_t, int);  
  
  
uint16_t htons(uint16_t);  
  
  
in_addr_t inet_addr(char const *);  
  
  
int close(int);  
  
  
void CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad(void)  
{  
  size_t data;  
    
  data = 0UL;  
  {  
    int recvResult;  
    struct sockaddr_in service;  
    char inputBuffer[26U];  
    int tmp;  
    ssize_t tmp_0;  
      
    int connectSocket = -1;  
      
    connectSocket = socket(2,1,6);  
      
    if (connectSocket == -1)   
                             goto ldv_4160; else ;  
      
    memset((void *)(& service),0,16UL);  
      
    service.sin_family = (unsigned short)2U;  
      
    service.sin_addr.s_addr = inet_addr("127.0.0.1");  
      
    service.sin_port = htons((unsigned short)27015);  
      
    tmp = connect(connectSocket,(struct sockaddr const *)(& service),16U);  
      
    if (tmp == -1)   
                   goto ldv_4160; else ;  
      
    tmp_0 = recv(connectSocket,(void *)(& inputBuffer),25UL,0);  
      
    recvResult = (int)tmp_0;  
      
    if (recvResult == -1 || recvResult == 0)   
                                             goto ldv_4160; else ;  
      
    inputBuffer[recvResult] = (char)0;  
      
    data = strtoul((char const *)(& inputBuffer),(char **)0,0);  
    ldv_4160:   
    ;  
      
    if (connectSocket != -1)   
                             close(connectSocket); else ;  
  }  
  {  
    char *myString;  
    size_t tmp_2;  
      
    tmp_2 = ldv_strlen_1("hello");  
      
    ;  
      
    if (tmp_2 < data) {  
        
      myString = (char *)malloc(data);  
        
      if (myString == (char *)0)   
                                 ldv_exit_2(-1); else ;  
        
      ldv_strcpy_3(myString,"hello");  
        
      printLine((char const *)myString);  
        
      free((void *)myString);  
    }  
    else   
         printLine("Input is less than the length of the source string");  
  }  
    
  return;  
}  
  
  
int main(int argc, char **argv)  
{  
  int __retres;  
  {  
    time_t tmp;  
      
    tmp = time((time_t *)0L);  
      
    srand((unsigned int)tmp);  
      
    printLine("Calling bad()...");  
      
    CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad();  
      
    printLine("Finished bad()");  
      
    __retres = 0;  
      
    goto return_label;  
  }  
    
  __retres = 0;  
  return_label:   
                return __retres;  
}  
  
  
static size_t ldv_strlen_1(char const *ldv_func_arg1)  
{  
  size_t tmp;  
    
  tmp = ldv_strlen(ldv_func_arg1);  
    
  return tmp;  
}  
  
  
static void ldv_exit_2(int ldv_func_arg1)  
{  
    
  ldv_exit();  
    
  return;  
}  
  
  
static char *ldv_strcpy_3(char * __restrict ldv_func_arg1, char const * __restrict ldv_func_arg2)  
{  
  char *tmp;  
    
  tmp = ldv_strcpy(ldv_func_arg1,ldv_func_arg2);  
    
  return tmp;  
}  
  
  
void *ldv_xmalloc(size_t size);  
  
  
int ldv_undef_int(void);  
  
  
int ldv_undef_int_positive(void);  
  
  
int ldv_asprintf(char **ptr);  
  
  
int ldv_asprintf(char **ptr)  
{  
  int __retres;  
  char *new;  
  int tmp_1;  
    
  tmp_1 = ldv_undef_int();  
    
  if (tmp_1 != 0) {  
    int tmp_0;  
      
    new = (char *)ldv_xmalloc(1UL);  
      
    *ptr = new;  
      
    tmp_0 = ldv_undef_int_positive();  
      
    __retres = tmp_0;  
      
    goto return_label;  
  }  
  else {  
      
    __retres = -1;  
      
    goto return_label;  
  }  
  return_label:   
                return __retres;  
}  
  
  
void abort(void);  
void assume_abort_if_not(int cond) {  
  if(!cond) {abort();}  
}  
  
  
void ldv_exit(void)  
{  
    
  assume_abort_if_not(0);  
    
  return;  
}  
  
  
void *ldv_xmalloc(size_t size);  
  
  
void *memcpy(void *, void const *, size_t);  
  
  
char *ldv_strdup(char const *s);  
  
  
char *ldv_strncpy(char *dest, char const *src, size_t n);  
  
  
char *ldv_strdup(char const *s)  
{  
  char *__retres;  
  char *new;  
  int tmp_2;  
    
  tmp_2 = ldv_undef_int();  
    
  if (tmp_2 != 0) {  
    void *tmp_0;  
    size_t tmp;  
    size_t tmp_1;  
      
    tmp = ldv_strlen(s);  
      
    tmp_0 = ldv_xmalloc(tmp);  
      
    new = (char *)tmp_0;  
      
    tmp_1 = ldv_strlen(s);  
      
    ;  
      
    ;  
      
    memcpy((void *)new,(void const *)s,tmp_1);  
      
    __retres = new;  
      
    goto return_label;  
  }  
  else {  
      
    __retres = (char *)0;  
      
    goto return_label;  
  }  
  return_label:   
                return __retres;  
}  
  
  
size_t ldv_strlen(char const *str)  
{  
  size_t __retres;  
  char const *s;  
    
  s = str;  
    
  goto ldv_1424;  
  ldv_1423:   
  ;  
    
  s += 1;  
  ldv_1424:   
  ;  
    
  if ((int)*s != 0)   
                    goto ldv_1423; else   
                                        goto ldv_1425;  
  ldv_1425:   
  ;  
    
  __retres = (unsigned long)((long)s - (long)str);  
    
  return __retres;  
}  
  
  
char *ldv_strncpy(char *dest, char const *src, size_t n)  
{  
  size_t i;  
    
  i = 0UL;  
    
  goto ldv_1433;  
  ldv_1432:   
  ;  
    
  *(dest + i) = *(src + i);  
    
  i += 1UL;  
  ldv_1433:   
  ;  
    
  if (i < n && (int)*(src + i) != 0)   
                                     goto ldv_1432; else   
                                                         goto ldv_1434;  
  ldv_1434:   
  ;  
    
  goto ldv_1436;  
  ldv_1435:   
  ;  
    
  *(dest + i) = (char)0;  
    
  i += 1UL;  
  ldv_1436:   
  ;  
    
  if (i < n)   
             goto ldv_1435; else   
                                 goto ldv_1437;  
  ldv_1437:   
  ;  
    
  return dest;  
}  
  
  
char *ldv_strcpy(char *dest, char const *src)  
{  
  size_t tmp;  
    
  tmp = ldv_strlen(src);  
    
  ;  
    
  ;  
    
  memcpy((void *)dest,(void const *)src,tmp);  
    
  return dest;  
}  
  
  
void *ldv_malloc(size_t size);  
  
  
void *ldv_calloc(size_t nmemb, size_t size);  
  
  
void *ldv_zalloc(size_t size);  
  
  
void ldv_free(void *s);  
  
  
void *ldv_realloc(void *ptr, size_t size);  
  
  
void *ldv_xzalloc(size_t size);  
  
  
  
  
  
  
  
  
void *ldv_reference_malloc(size_t size);  
  
  
void *ldv_reference_calloc(size_t nmemb, size_t size);  
  
  
void *ldv_reference_zalloc(size_t size);  
  
  
void ldv_reference_free(void *s);  
  
  
void *ldv_reference_realloc(void *ptr, size_t size);  
  
  
void *ldv_reference_xmalloc(size_t size);  
  
  
void *ldv_reference_xzalloc(size_t size);  
  
  
  
  
  
  
  
  
  
  
void *ldv_malloc(size_t size)  
{  
  void *tmp;  
    
  tmp = ldv_reference_malloc(size);  
    
  return tmp;  
}  
  
  
void *ldv_calloc(size_t nmemb, size_t size)  
{  
  void *tmp;  
    
  tmp = ldv_reference_calloc(nmemb,size);  
    
  return tmp;  
}  
  
  
void *ldv_zalloc(size_t size)  
{  
  void *tmp;  
    
  tmp = ldv_reference_zalloc(size);  
    
  return tmp;  
}  
  
  
void ldv_free(void *s)  
{  
    
  ldv_reference_free(s);  
    
  return;  
}  
  
  
void *ldv_xmalloc(size_t size)  
{  
  void *tmp;  
    
  tmp = ldv_reference_xmalloc(size);  
    
  return tmp;  
}  
  
  
void *ldv_xzalloc(size_t size)  
{  
  void *tmp;  
    
  tmp = ldv_reference_xzalloc(size);  
    
  return tmp;  
}  
  
  
  
  
  
  
  
  
  
  
void *ldv_realloc(void *ptr, size_t size)  
{  
  void *tmp;  
    
  tmp = ldv_reference_realloc(ptr,size);  
    
  return tmp;  
}  
  
  
void abort(void);  
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  
void reach_error() { __assert_fail("0", "CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i", 1371, "reach_error"); }  
  
  
void ldv_error(void);  
  
  
void ldv_error(void)  
{  
    
  {reach_error();}  
    
  return;  
}  
  
  
  
  
  
int ldv_undef_long(void);  
  
  
unsigned int ldv_undef_uint(void);  
  
  
unsigned long ldv_undef_ulong(void);  
  
  
unsigned long long ldv_undef_ulonglong(void);  
  
  
  
  
int ldv_undef_int_negative(void);  
  
  
int ldv_undef_int_nonpositive(void);  
  
  
  
  
int __VERIFIER_nondet_int(void);  
  
  
long __VERIFIER_nondet_long(void);  
  
  
unsigned int __VERIFIER_nondet_uint(void);  
  
  
unsigned long __VERIFIER_nondet_ulong(void);  
  
  
unsigned long long __VERIFIER_nondet_ulonglong(void);  
  
  
  
  
int ldv_undef_int(void)  
{  
  int tmp;  
    
  tmp = __VERIFIER_nondet_int();  
    
  return tmp;  
}  
  
  
int ldv_undef_long(void)  
{  
  int __retres;  
  long tmp;  
    
  tmp = __VERIFIER_nondet_long();  
    
  __retres = (int)tmp;  
    
  return __retres;  
}  
  
  
unsigned int ldv_undef_uint(void)  
{  
  unsigned int tmp;  
    
  tmp = __VERIFIER_nondet_uint();  
    
  return tmp;  
}  
  
  
  
  
unsigned long ldv_undef_ulong(void)  
{  
  unsigned long tmp;  
    
  tmp = __VERIFIER_nondet_ulong();  
    
  return tmp;  
}  
  
  
unsigned long long ldv_undef_ulonglong(void)  
{  
  unsigned long long tmp;  
    
  tmp = __VERIFIER_nondet_ulonglong();  
    
  return tmp;  
}  
  
  
int ldv_undef_int_positive(void)  
{  
    
  int ret = ldv_undef_int();  
    
  assume_abort_if_not(ret > 0);  
    
  return ret;  
}  
  
  
int ldv_undef_int_negative(void)  
{  
    
  int ret = ldv_undef_int();  
    
  assume_abort_if_not(ret < 0);  
    
  return ret;  
}  
  
  
int ldv_undef_int_nonpositive(void)  
{  
    
  int ret = ldv_undef_int();  
    
  assume_abort_if_not(ret <= 0);  
    
  return ret;  
}  
  
  
  
  
  
  
void *calloc(size_t, size_t);  
  
  
void *ldv_reference_malloc(size_t size)  
{  
  void *__retres;  
  void *res;  
  int tmp;  
    
  tmp = ldv_undef_int();  
    
  if (tmp != 0) {  
      
    res = malloc(size);  
      
    assume_abort_if_not(res != (void *)0);  
      
    __retres = res;  
      
    goto return_label;  
  }  
  else {  
      
    __retres = (void *)0;  
      
    goto return_label;  
  }  
  return_label:   
                return __retres;  
}  
  
  
void *ldv_reference_calloc(size_t nmemb, size_t size)  
{  
  void *tmp;  
    
  tmp = calloc(nmemb,size);  
    
  return tmp;  
}  
  
  
void *ldv_reference_zalloc(size_t size)  
{  
  void *tmp;  
    
  tmp = calloc(1UL,size);  
    
  return tmp;  
}  
  
  
void ldv_reference_free(void *s)  
{  
    
  free(s);  
    
  return;  
}  
  
  
void *ldv_reference_realloc(void *ptr, size_t size)  
{  
  void *__retres;  
  void *res;  
  int tmp;  
    
  if (ptr != (void *)0 && size == 0UL) {  
      
    free(ptr);  
      
    __retres = (void *)0;  
      
    goto return_label;  
  }  
  else ;  
    
  if (ptr == (void *)0) {  
      
    res = malloc(size);  
      
    __retres = res;  
      
    goto return_label;  
  }  
  else ;  
    
  tmp = ldv_undef_int();  
    
  if (tmp != 0) {  
      
    res = malloc(size);  
      
    assume_abort_if_not(res != (void *)0);  
      
    memcpy(res,(void const *)ptr,size);  
      
    free(ptr);  
      
    __retres = res;  
      
    goto return_label;  
  }  
  else {  
      
    __retres = (void *)0;  
      
    goto return_label;  
  }  
  return_label:   
                return __retres;  
}  
  
  
void *ldv_reference_xmalloc(size_t size)  
{  
  void *res;  
    
  res = malloc(size);  
    
  assume_abort_if_not(res != (void *)0);  
    
  return res;  
}  
  
  
void *ldv_reference_xzalloc(size_t size)  
{  
  void *res;  
    
  res = calloc(1UL,size);  
    
  assume_abort_if_not(res != (void *)0);  
    
  return res;  
}  
  
  
  
  
  
  
  
  
  
  

Log not available

Statistics NameStatistics ValueAdditional Value
Parallel Algorithm statistics
Number of algorithms used        5
Successful analysis /opt/cpachecker/config/components/smgAnalysis-symEx.properties
Statistics for /opt/cpachecker/config/components/smgAnalysis-symEx.properties
==============================================================================
SMGCPA statistics
Number of variables per state                     17.51 sum: 613, count: 35, min: 0, max: 25
Number of global variables per state              8.51 sum: 298, count: 35, min: 0, max: 10
Time for solving constraints                          0.361s
	  Time for independent computation                    0.010s
	  Time for SMT check                                  0.007s
	  Time for resolving definites                        0.028s
Cache lookups                                           13
Direct cache hits                                        3
Direct cache lookup time                              0.001s
Number of assumptions                                   20
Number of deterministic assumptions                      0
Level of Determinism                              0%
Number of list materializations :                 0
Total time spent on materialization :             0ms
Max time spent on materialization :               0ms
Number of 0+ materializations                            0
Total time spent on 0+ materialization :          0ms
Max time spent on 0+ materialization :            0ms
Number of lists abstracted in total :             0
Total time spent on list abstraction :            0ms
Max time spent on list abstraction :              0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states                                  1
Total time for successor computation                  0.010s
Total time for strengthen operator                    0.129s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states                                  1
Total time for successor computation                  0.005s
Total time for strengthen operator                    0.086s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states                                  1
Total time for successor computation                  0.002s
Total time for strengthen operator                    0.074s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions      0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states                                  1
Total time for successor computation                  0.016s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions      0
CPA algorithm statistics
Number of iterations            31
Max size of waitlist            5
Average size of waitlist        2
Number of computed successors   35
Max successors for one state    2
Number of times merged          0
Number of times stopped         1
Number of times breaked         1
Total time for CPA algorithm         1.256s Max:     1.256s
	  Time for choose from waitlist      0.001s
	  Time for precision adjustment      0.042s
	  Time for transfer relation         1.174s
	  Time for stop operator             0.037s
	  Time for adding to reached set     0.000s
Statistics for /opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties
=====================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties     0.002s
SMGCPA statistics
Number of variables per state                     15.55 sum: 342, count: 22, min: 0, max: 20
Number of global variables per state              8.14 sum: 179, count: 22, min: 0, max: 9
Time for solving constraints                          0.285s
	  Time for independent computation                    0.002s
	  Time for SMT check                                  0.006s
	  Time for resolving definites                        0.046s
Cache lookups                                            9
Direct cache hits                                        1
Direct cache lookup time                              0.000s
Number of assumptions                                   12
Number of deterministic assumptions                      0
Level of Determinism                              0%
Number of list materializations :                 0
Total time spent on materialization :             0ms
Max time spent on materialization :               0ms
Number of 0+ materializations                            0
Total time spent on 0+ materialization :          0ms
Max time spent on 0+ materialization :            0ms
Number of lists abstracted in total :             0
Total time spent on list abstraction :            0ms
Max time spent on list abstraction :              0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states                                  1
Total time for successor computation                  0.029s
Total time for strengthen operator                    0.146s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states                                  1
Total time for successor computation                  0.010s
Total time for strengthen operator                    0.116s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states                                  1
Total time for successor computation                  0.004s
Total time for strengthen operator                    0.139s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions      0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states                                  1
Total time for successor computation                  0.008s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions      0
CPA algorithm statistics
Number of iterations            18
Max size of waitlist            5
Average size of waitlist        1
Number of computed successors   21
Max successors for one state    2
Number of times merged          0
Number of times stopped         0
Number of times breaked         0
Total time for CPA algorithm         1.196s Max:     1.196s
	  Time for choose from waitlist      0.000s
	  Time for precision adjustment      0.072s
	  Time for transfer relation         1.113s
	  Time for stop operator             0.009s
	  Time for adding to reached set     0.000s
Statistics for /opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties
===============================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties     0.429s
SMGCPA statistics
Number of variables per state                     17.36 sum: 573, count: 33, min: 0, max: 25
Number of global variables per state              8.48 sum: 280, count: 33, min: 0, max: 10
Number of assumptions                                   16
Number of deterministic assumptions                      0
Level of Determinism                              0%
Number of list materializations :                 0
Total time spent on materialization :             0ms
Max time spent on materialization :               0ms
Number of 0+ materializations                            0
Total time spent on 0+ materialization :          0ms
Max time spent on 0+ materialization :            0ms
Number of lists abstracted in total :             0
Total time spent on list abstraction :            0ms
Max time spent on list abstraction :              0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states                                  1
Total time for successor computation                  0.028s
Total time for strengthen operator                    0.210s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states                                  1
Total time for successor computation                  0.025s
Total time for strengthen operator                    0.116s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states                                  1
Total time for successor computation                  0.005s
Total time for strengthen operator                    0.055s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions      0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states                                  1
Total time for successor computation                  0.007s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions      0
CPA algorithm statistics
Number of iterations            28
Max size of waitlist            5
Average size of waitlist        2
Number of computed successors   34
Max successors for one state    2
Number of times merged          0
Number of times stopped         2
Number of times breaked         1
Total time for CPA algorithm         0.913s Max:     0.913s
	  Time for choose from waitlist      0.000s
	  Time for precision adjustment      0.064s
	  Time for transfer relation         0.776s
	  Time for stop operator             0.057s
	  Time for adding to reached set     0.008s
Counterexample-Check Algorithm statistics
Number of counterexample checks    1
Number of infeasible paths         0 0%
Time for counterexample checks         1.642s
Statistics for /opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties
======================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties     0.432s
SMGCPA statistics
Number of variables per state                     19.05 sum: 819, count: 43, min: 0, max: 28
Number of global variables per state              8.74 sum: 376, count: 43, min: 0, max: 10
Number of assumptions                                   24
Number of deterministic assumptions                      0
Level of Determinism                              0%
Number of list materializations :                 0
Total time spent on materialization :             0ms
Max time spent on materialization :               0ms
Number of 0+ materializations                            0
Total time spent on 0+ materialization :          0ms
Max time spent on 0+ materialization :            0ms
Number of lists abstracted in total :             0
Total time spent on list abstraction :            0ms
Max time spent on list abstraction :              0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states                                  1
Total time for successor computation                  0.024s
Total time for strengthen operator                    0.192s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states                                  1
Total time for successor computation                  0.003s
Total time for strengthen operator                    0.169s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states                                  1
Total time for successor computation                  0.011s
Total time for strengthen operator                    0.082s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions      0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states                                  1
Total time for successor computation                  0.004s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions      0
CPA algorithm statistics
Number of iterations            38
Max size of waitlist            5
Average size of waitlist        2
Number of computed successors   44
Max successors for one state    2
Number of times merged          0
Number of times stopped         2
Number of times breaked         1
Total time for CPA algorithm         0.964s Max:     0.964s
	  Time for choose from waitlist      0.001s
	  Time for precision adjustment      0.070s
	  Time for transfer relation         0.787s
	  Time for stop operator             0.087s
	  Time for adding to reached set     0.003s
Counterexample-Check Algorithm statistics
Number of counterexample checks    1
Number of infeasible paths         0 0%
Time for counterexample checks         1.583s
Statistics for /opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties
=========================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties     0.304s
SMGCPA statistics
Number of variables per state                     15.74 sum: 362, count: 23, min: 0, max: 20
Number of global variables per state              8.17 sum: 188, count: 23, min: 0, max: 9
Time for solving constraints                          0.245s
	  Time for independent computation                    0.009s
	  Time for SMT check                                  0.029s
	  Time for resolving definites                        0.066s
Cache lookups                                            9
Direct cache hits                                        0
Direct cache lookup time                              0.000s
Number of assumptions                                   12
Number of deterministic assumptions                      0
Level of Determinism                              0%
Number of list materializations :                 0
Total time spent on materialization :             0ms
Max time spent on materialization :               0ms
Number of 0+ materializations                            0
Total time spent on 0+ materialization :          0ms
Max time spent on 0+ materialization :            0ms
Number of lists abstracted in total :             0
Total time spent on list abstraction :            0ms
Max time spent on list abstraction :              0ms
Total time spent on searching for list abstractions : 0ms
Max time spent on searching a single list abstractions : 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states                                  1
Total time for successor computation                  0.012s
Total time for strengthen operator                    0.304s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states                                  1
Total time for successor computation                  0.000s
Total time for strengthen operator                    0.198s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions      0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states                                  1
Total time for successor computation                  0.002s
Total time for strengthen operator                    0.119s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions      0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states                                  1
Total time for successor computation                  0.001s
Automaton transfers with branching                0
Automaton transfer successors                     1.00 sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions      0
CPA algorithm statistics
Number of iterations            18
Max size of waitlist            5
Average size of waitlist        1
Number of computed successors   22
Max successors for one state    2
Number of times merged          0
Number of times stopped         0
Number of times breaked         1
Total time for CPA algorithm         1.275s Max:     1.275s
	  Time for choose from waitlist      0.001s
	  Time for precision adjustment      0.049s
	  Time for transfer relation         1.195s
	  Time for stop operator             0.014s
	  Time for adding to reached set     0.002s
Counterexample-Check Algorithm statistics
Number of counterexample checks    1
Number of infeasible paths         0 0%
Time for counterexample checks         1.272s
Other statistics
================
Code Coverage
	  Function coverage      0.050
	  Visited lines          134
	  Total lines            507
	  Line coverage          0.264
	  Visited conditions     11
	  Total conditions       66
	  Condition coverage     0.167
CPAchecker general statistics
Number of program locations                       778
Number of CFA edges (per node)                         765 count: 778, min: 0, max: 8, avg: 0.98
Number of relevant variables                      111
Number of functions                               80
Number of loops (and loop nodes)                         6 sum: 52, min: 5, max: 14, avg: 8.67
Size of reached set             35
	  Number of reached locations   30 4%
		    Avg states per location     1
		    Max states per location     4 at node N378
	  Number of reached functions   4 5%
	  Number of partitions          30
		    Avg size of partitions      1
		    Max size of partitions      4 with key [N378 before line 961, Function CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad called from node N406, stack depth 2 [73fafd4], stack [main, CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad], 20]
	  Number of target states       1
	  Size of final wait list       4
Time for analysis setup          7.745s
	  Time for loading CPAs          2.632s
	  Time for loading parser        0.569s
	  Time for CFA construction      3.404s
		    Time for parsing file(s)     0.773s
		    Time for AST to CFA          0.970s
		    Time for CFA sanity check    0.148s
		    Time for post-processing     1.384s
		    Time for loop structure      0.039s
		    Time for AST structure       0.000s
		    Time for CFA export          2.156s
			      Time for function pointers resolving            0.021s
				        Function calls via function pointers             1 count: 1, min: 1, max: 1, avg: 1.00
				        Instrumented function pointer calls              0 count: 1, min: 0, max: 0, avg: 0.00
				        Function calls with function pointer arguments        0 count: 1, min: 0, max: 0, avg: 0.00
				        Instrumented function pointer arguments          0 count: 1, min: 0, max: 0, avg: 0.00
			      Time for classifying variables                  0.416s
				        Time for collecting variables                 0.250s
				        Time for solving dependencies                 0.008s
				        Time for building hierarchy                   0.000s
				        Time for building classification              0.095s
				        Time for exporting data                       0.063s
Time for Analysis                2.661s
CPU time for analysis            7.500s
Time for analyzing result        0.002s
Total time for CPAchecker       10.409s
Total CPU time for CPAchecker   21.010s
Time for statistics              0.215s
Time for Garbage Collector       0.562s in 4 runs
Garbage Collector(s) used    PS MarkSweep, PS Scavenge
Used heap memory                191MB (   182 MiB) max;     98MB (    94 MiB) avg;    211MB (   201 MiB) peak
Used non-heap memory             54MB (    52 MiB) max;     36MB (    34 MiB) avg;     56MB (    53 MiB) peak
Used in PS Old Gen pool          20MB (    19 MiB) max;      9MB (     8 MiB) avg;     20MB (    19 MiB) peak
Allocated heap memory          1002MB (   956 MiB) max;   1002MB (   956 MiB) avg
Allocated non-heap memory        57MB (    55 MiB) max;     38MB (    37 MiB) avg
Total process virtual memory   5609MB (  5350 MiB) max;   4716MB (  4498 MiB) avg

        

Statistics Name	Statistics Value	Additional Value
Parallel Algorithm statistics
Number of algorithms used	5
Successful analysis	/opt/cpachecker/config/components/smgAnalysis-symEx.properties
Statistics for	/opt/cpachecker/config/components/smgAnalysis-symEx.properties
==============================================================================
SMGCPA statistics
Number of variables per state	17.51	sum: 613, count: 35, min: 0, max: 25
Number of global variables per state	8.51	sum: 298, count: 35, min: 0, max: 10
Time for solving constraints	0.361s
Time for independent computation	0.010s
Time for SMT check	0.007s
Time for resolving definites	0.028s
Cache lookups	13
Direct cache hits	3
Direct cache lookup time	0.001s
Number of assumptions	20
Number of deterministic assumptions	0
Level of Determinism	0%
Number of list materializations	: 0
Total time spent on materialization	: 0ms
Max time spent on materialization	: 0ms
Number of 0+ materializations	0
Total time spent on 0+ materialization	: 0ms
Max time spent on 0+ materialization	: 0ms
Number of lists abstracted in total	: 0
Total time spent on list abstraction	: 0ms
Max time spent on list abstraction	: 0ms
Total time spent on searching for list abstractions	: 0ms
Max time spent on searching a single list abstractions	: 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states	1
Total time for successor computation	0.010s
Total time for strengthen operator	0.129s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states	1
Total time for successor computation	0.005s
Total time for strengthen operator	0.086s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states	1
Total time for successor computation	0.002s
Total time for strengthen operator	0.074s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions	0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states	1
Total time for successor computation	0.016s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 231, count: 231, min: 1, max: 1 [1 x 231]
Number of states with assumption transitions	0
CPA algorithm statistics
Number of iterations	31
Max size of waitlist	5
Average size of waitlist	2
Number of computed successors	35
Max successors for one state	2
Number of times merged	0
Number of times stopped	1
Number of times breaked	1
Total time for CPA algorithm	1.256s	Max: 1.256s
Time for choose from waitlist	0.001s
Time for precision adjustment	0.042s
Time for transfer relation	1.174s
Time for stop operator	0.037s
Time for adding to reached set	0.000s
Statistics for	/opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties
=====================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-concrete-memory-access.properties	0.002s
SMGCPA statistics
Number of variables per state	15.55	sum: 342, count: 22, min: 0, max: 20
Number of global variables per state	8.14	sum: 179, count: 22, min: 0, max: 9
Time for solving constraints	0.285s
Time for independent computation	0.002s
Time for SMT check	0.006s
Time for resolving definites	0.046s
Cache lookups	9
Direct cache hits	1
Direct cache lookup time	0.000s
Number of assumptions	12
Number of deterministic assumptions	0
Level of Determinism	0%
Number of list materializations	: 0
Total time spent on materialization	: 0ms
Max time spent on materialization	: 0ms
Number of 0+ materializations	0
Total time spent on 0+ materialization	: 0ms
Max time spent on 0+ materialization	: 0ms
Number of lists abstracted in total	: 0
Total time spent on list abstraction	: 0ms
Max time spent on list abstraction	: 0ms
Total time spent on searching for list abstractions	: 0ms
Max time spent on searching a single list abstractions	: 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states	1
Total time for successor computation	0.029s
Total time for strengthen operator	0.146s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states	1
Total time for successor computation	0.010s
Total time for strengthen operator	0.116s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states	1
Total time for successor computation	0.004s
Total time for strengthen operator	0.139s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions	0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states	1
Total time for successor computation	0.008s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 215, count: 215, min: 1, max: 1 [1 x 215]
Number of states with assumption transitions	0
CPA algorithm statistics
Number of iterations	18
Max size of waitlist	5
Average size of waitlist	1
Number of computed successors	21
Max successors for one state	2
Number of times merged	0
Number of times stopped	0
Number of times breaked	0
Total time for CPA algorithm	1.196s	Max: 1.196s
Time for choose from waitlist	0.000s
Time for precision adjustment	0.072s
Time for transfer relation	1.113s
Time for stop operator	0.009s
Time for adding to reached set	0.000s
Statistics for	/opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties
===============================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-abstract-concrete-values-with-cex.properties	0.429s
SMGCPA statistics
Number of variables per state	17.36	sum: 573, count: 33, min: 0, max: 25
Number of global variables per state	8.48	sum: 280, count: 33, min: 0, max: 10
Number of assumptions	16
Number of deterministic assumptions	0
Level of Determinism	0%
Number of list materializations	: 0
Total time spent on materialization	: 0ms
Max time spent on materialization	: 0ms
Number of 0+ materializations	0
Total time spent on 0+ materialization	: 0ms
Max time spent on 0+ materialization	: 0ms
Number of lists abstracted in total	: 0
Total time spent on list abstraction	: 0ms
Max time spent on list abstraction	: 0ms
Total time spent on searching for list abstractions	: 0ms
Max time spent on searching a single list abstractions	: 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states	1
Total time for successor computation	0.028s
Total time for strengthen operator	0.210s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states	1
Total time for successor computation	0.025s
Total time for strengthen operator	0.116s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states	1
Total time for successor computation	0.005s
Total time for strengthen operator	0.055s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions	0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states	1
Total time for successor computation	0.007s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 230, count: 230, min: 1, max: 1 [1 x 230]
Number of states with assumption transitions	0
CPA algorithm statistics
Number of iterations	28
Max size of waitlist	5
Average size of waitlist	2
Number of computed successors	34
Max successors for one state	2
Number of times merged	0
Number of times stopped	2
Number of times breaked	1
Total time for CPA algorithm	0.913s	Max: 0.913s
Time for choose from waitlist	0.000s
Time for precision adjustment	0.064s
Time for transfer relation	0.776s
Time for stop operator	0.057s
Time for adding to reached set	0.008s
Counterexample-Check Algorithm statistics
Number of counterexample checks	1
Number of infeasible paths	0	0%
Time for counterexample checks	1.642s
Statistics for	/opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties
======================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgValueAnalysis-with-cex.properties	0.432s
SMGCPA statistics
Number of variables per state	19.05	sum: 819, count: 43, min: 0, max: 28
Number of global variables per state	8.74	sum: 376, count: 43, min: 0, max: 10
Number of assumptions	24
Number of deterministic assumptions	0
Level of Determinism	0%
Number of list materializations	: 0
Total time spent on materialization	: 0ms
Max time spent on materialization	: 0ms
Number of 0+ materializations	0
Total time spent on 0+ materialization	: 0ms
Max time spent on 0+ materialization	: 0ms
Number of lists abstracted in total	: 0
Total time spent on list abstraction	: 0ms
Max time spent on list abstraction	: 0ms
Total time spent on searching for list abstractions	: 0ms
Max time spent on searching a single list abstractions	: 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states	1
Total time for successor computation	0.024s
Total time for strengthen operator	0.192s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states	1
Total time for successor computation	0.003s
Total time for strengthen operator	0.169s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states	1
Total time for successor computation	0.011s
Total time for strengthen operator	0.082s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions	0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states	1
Total time for successor computation	0.004s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 244, count: 244, min: 1, max: 1 [1 x 244]
Number of states with assumption transitions	0
CPA algorithm statistics
Number of iterations	38
Max size of waitlist	5
Average size of waitlist	2
Number of computed successors	44
Max successors for one state	2
Number of times merged	0
Number of times stopped	2
Number of times breaked	1
Total time for CPA algorithm	0.964s	Max: 0.964s
Time for choose from waitlist	0.001s
Time for precision adjustment	0.070s
Time for transfer relation	0.787s
Time for stop operator	0.087s
Time for adding to reached set	0.003s
Counterexample-Check Algorithm statistics
Number of counterexample checks	1
Number of infeasible paths	0	0%
Time for counterexample checks	1.583s
Statistics for	/opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties
=========================================================================================================
Time spent in analysis thread /opt/cpachecker/config/components/smgAnalysis-symEx-overapproximating-with-cex.properties	0.304s
SMGCPA statistics
Number of variables per state	15.74	sum: 362, count: 23, min: 0, max: 20
Number of global variables per state	8.17	sum: 188, count: 23, min: 0, max: 9
Time for solving constraints	0.245s
Time for independent computation	0.009s
Time for SMT check	0.029s
Time for resolving definites	0.066s
Cache lookups	9
Direct cache hits	0
Direct cache lookup time	0.000s
Number of assumptions	12
Number of deterministic assumptions	0
Level of Determinism	0%
Number of list materializations	: 0
Total time spent on materialization	: 0ms
Max time spent on materialization	: 0ms
Number of 0+ materializations	0
Total time spent on 0+ materialization	: 0ms
Max time spent on 0+ materialization	: 0ms
Number of lists abstracted in total	: 0
Total time spent on list abstraction	: 0ms
Max time spent on list abstraction	: 0ms
Total time spent on searching for list abstractions	: 0ms
Max time spent on searching a single list abstractions	: 0ms
AutomatonAnalysis (SMGCPADEREF) statistics
Number of states	1
Total time for successor computation	0.012s
Total time for strengthen operator	0.304s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAFREE) statistics
Number of states	1
Total time for successor computation	0.000s
Total time for strengthen operator	0.198s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions	0
AutomatonAnalysis (SMGCPAMEMTRACK) statistics
Number of states	1
Total time for successor computation	0.002s
Total time for strengthen operator	0.119s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions	0
AutomatonAnalysis (svcompTerminatingFunctions) statistics
Number of states	1
Total time for successor computation	0.001s
Automaton transfers with branching	0
Automaton transfer successors	1.00	sum: 216, count: 216, min: 1, max: 1 [1 x 216]
Number of states with assumption transitions	0
CPA algorithm statistics
Number of iterations	18
Max size of waitlist	5
Average size of waitlist	1
Number of computed successors	22
Max successors for one state	2
Number of times merged	0
Number of times stopped	0
Number of times breaked	1
Total time for CPA algorithm	1.275s	Max: 1.275s
Time for choose from waitlist	0.001s
Time for precision adjustment	0.049s
Time for transfer relation	1.195s
Time for stop operator	0.014s
Time for adding to reached set	0.002s
Counterexample-Check Algorithm statistics
Number of counterexample checks	1
Number of infeasible paths	0	0%
Time for counterexample checks	1.272s
Other statistics
================
Code Coverage
Function coverage	0.050
Visited lines	134
Total lines	507
Line coverage	0.264
Visited conditions	11
Total conditions	66
Condition coverage	0.167
CPAchecker general statistics
Number of program locations	778
Number of CFA edges (per node)	765	count: 778, min: 0, max: 8, avg: 0.98
Number of relevant variables	111
Number of functions	80
Number of loops (and loop nodes)	6	sum: 52, min: 5, max: 14, avg: 8.67
Size of reached set	35
Number of reached locations	30	4%
Avg states per location	1
Max states per location	4	at node N378
Number of reached functions	4	5%
Number of partitions	30
Avg size of partitions	1
Max size of partitions	4	with key [N378 before line 961, Function CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad called from node N406, stack depth 2 [73fafd4], stack [main, CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad], 20]
Number of target states	1
Size of final wait list	4
Time for analysis setup	7.745s
Time for loading CPAs	2.632s
Time for loading parser	0.569s
Time for CFA construction	3.404s
Time for parsing file(s)	0.773s
Time for AST to CFA	0.970s
Time for CFA sanity check	0.148s
Time for post-processing	1.384s
Time for loop structure	0.039s
Time for AST structure	0.000s
Time for CFA export	2.156s
Time for function pointers resolving	0.021s
Function calls via function pointers	1	count: 1, min: 1, max: 1, avg: 1.00
Instrumented function pointer calls	0	count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments	0	count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables	0.416s
Time for collecting variables	0.250s
Time for solving dependencies	0.008s
Time for building hierarchy	0.000s
Time for building classification	0.095s
Time for exporting data	0.063s
Time for Analysis	2.661s
CPU time for analysis	7.500s
Time for analyzing result	0.002s
Total time for CPAchecker	10.409s
Total CPU time for CPAchecker	21.010s
Time for statistics	0.215s
Time for Garbage Collector	0.562s	in 4 runs
Garbage Collector(s) used	PS MarkSweep, PS Scavenge
Used heap memory	191MB ( 182 MiB) max; 98MB ( 94 MiB) avg; 211MB ( 201 MiB) peak
Used non-heap memory	54MB ( 52 MiB) max; 36MB ( 34 MiB) avg; 56MB ( 53 MiB) peak
Used in PS Old Gen pool	20MB ( 19 MiB) max; 9MB ( 8 MiB) avg; 20MB ( 19 MiB) peak
Allocated heap memory	1002MB ( 956 MiB) max; 1002MB ( 956 MiB) avg
Allocated non-heap memory	57MB ( 55 MiB) max; 38MB ( 37 MiB) avg
Total process virtual memory	5609MB ( 5350 MiB) max; 4716MB ( 4498 MiB) avg

#Configuration NameConfiguration Value
1analysis.entryFunction  main
2analysis.programNames  CWE789-1/CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i
3analysis.useParallelAnalyses  true
4cfa.findLiveVariables  true
5cfa.simplifyCfa  false
6counterexample.export.compressWitness  false
7counterexample.export.graphml  witness.graphml
8counterexample.export.yaml  witness.yml
9cpa.arg.compressWitness  false
10cpa.arg.yamlProofWitness  witness.yml
11cpa.callstack.unsupportedFunctions  pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow,_longjmp,longjmp,siglongjmp
12cpa.smg2.handleUnknownFunctions  ASSUME_EXTERNAL_ALLOCATED
13language  C
14limits.time.cpu  30
15parallelAlgorithm.configFiles  smgAnalysis-symEx.properties, smgAnalysis-symEx-concrete-memory-access.properties, smgValueAnalysis-abstract-concrete-values-with-cex.properties, smgValueAnalysis-with-cex.properties, smgAnalysis-symEx-overapproximating-with-cex.properties
16specification  properties/valid-memsafety.prp

        

#	Configuration Name	Configuration Value
1	analysis.entryFunction	main
2	analysis.programNames	CWE789-1/CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i
3	analysis.useParallelAnalyses	true
4	cfa.findLiveVariables	true
5	cfa.simplifyCfa	false
6	counterexample.export.compressWitness	false
7	counterexample.export.graphml	witness.graphml
8	counterexample.export.yaml	witness.yml
9	cpa.arg.compressWitness	false
10	cpa.arg.yamlProofWitness	witness.yml
11	cpa.callstack.unsupportedFunctions	pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow,_longjmp,longjmp,siglongjmp
12	cpa.smg2.handleUnknownFunctions	ASSUME_EXTERNAL_ALLOCATED
13	language	C
14	limits.time.cpu	30
15	parallelAlgorithm.configFiles	smgAnalysis-symEx.properties, smgAnalysis-symEx-concrete-memory-access.properties, smgValueAnalysis-abstract-concrete-values-with-cex.properties, smgValueAnalysis-with-cex.properties, smgAnalysis-symEx-overapproximating-with-cex.properties
16	specification	properties/valid-memsafety.prp

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

Source: {{dependency.repository}}

License:

Full text of license

{{dependencies.licenses[dependency.licenseId]}}

Report for CWE789-1/CWE789_Uncontrolled_Mem_Alloc---s01---CWE789_Uncontrolled_Mem_Alloc__malloc_char_connect_socket_01_bad.i

About

{{dependency.name}} {{dependency.version}}